Left Termination of the query pattern reach_in_4(g, g, g, g) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

reach(X, Y, E, L) :- member(.(X, .(Y, [])), E).
reach(X, Z, E, L) :- ','(member1(.(X, .(Y, [])), E), ','(member(Y, L), ','(delete(Y, L, V1), reach(Y, Z, E, V1)))).
member(H, .(H, L)).
member(X, .(H, L)) :- member(X, L).
member1(H, .(H, L)).
member1(X, .(H, L)) :- member1(X, L).
delete(X, .(X, Y), Y).
delete(X, .(H, T1), .(H, T2)) :- delete(X, T1, T2).

Queries:

reach(g,g,g,g).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
reach_in: (b,b,b,b) (f,b,b,b)
member_in: (b,b) (f,b)
member1_in: (b,b)
delete_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

REACH_IN_GGGG(X, Y, E, L) → U1_GGGG(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Y, E, L) → MEMBER_IN_GG(.(X, .(Y, [])), E)
MEMBER_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Z, E, L) → MEMBER1_IN_GG(.(X, .(Y, [])), E)
MEMBER1_IN_GG(X, .(H, L)) → U7_GG(X, H, L, member1_in_gg(X, L))
MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)
U2_GGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_ag(Y, L))
U2_GGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → MEMBER_IN_AG(Y, L)
MEMBER_IN_AG(X, .(H, L)) → U6_AG(X, H, L, member_in_ag(X, L))
MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)
U3_GGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U3_GGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → DELETE_IN_AGA(Y, L, V1)
DELETE_IN_AGA(X, .(H, T1), .(H, T2)) → U8_AGA(X, H, T1, T2, delete_in_aga(X, T1, T2))
DELETE_IN_AGA(X, .(H, T1), .(H, T2)) → DELETE_IN_AGA(X, T1, T2)
U4_GGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_GGGG(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → REACH_IN_AGGG(Y, Z, E, V1)
REACH_IN_AGGG(X, Y, E, L) → U1_AGGG(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
REACH_IN_AGGG(X, Y, E, L) → MEMBER_IN_GG(.(X, .(Y, [])), E)
REACH_IN_AGGG(X, Z, E, L) → U2_AGGG(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
REACH_IN_AGGG(X, Z, E, L) → MEMBER1_IN_GG(.(X, .(Y, [])), E)
U2_AGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_AGGG(X, Z, E, L, Y, member_in_ag(Y, L))
U2_AGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → MEMBER_IN_AG(Y, L)
U3_AGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_AGGG(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U3_AGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → DELETE_IN_AGA(Y, L, V1)
U4_AGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_AGGG(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U4_AGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → REACH_IN_AGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)
U4_AGGG(x1, x2, x3, x4, x5, x6)  =  U4_AGGG(x2, x3, x6)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x2, x3, x4, x5)
U5_AGGG(x1, x2, x3, x4, x5)  =  U5_AGGG(x5)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x4)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
REACH_IN_GGGG(x1, x2, x3, x4)  =  REACH_IN_GGGG(x1, x2, x3, x4)
U1_GGGG(x1, x2, x3, x4, x5)  =  U1_GGGG(x5)
U3_GGGG(x1, x2, x3, x4, x5, x6)  =  U3_GGGG(x2, x3, x4, x6)
U8_AGA(x1, x2, x3, x4, x5)  =  U8_AGA(x5)
U5_GGGG(x1, x2, x3, x4, x5)  =  U5_GGGG(x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
U7_GG(x1, x2, x3, x4)  =  U7_GG(x4)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x4)
DELETE_IN_AGA(x1, x2, x3)  =  DELETE_IN_AGA(x2)
U4_GGGG(x1, x2, x3, x4, x5, x6)  =  U4_GGGG(x2, x3, x6)
U1_AGGG(x1, x2, x3, x4, x5)  =  U1_AGGG(x5)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

REACH_IN_GGGG(X, Y, E, L) → U1_GGGG(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Y, E, L) → MEMBER_IN_GG(.(X, .(Y, [])), E)
MEMBER_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Z, E, L) → MEMBER1_IN_GG(.(X, .(Y, [])), E)
MEMBER1_IN_GG(X, .(H, L)) → U7_GG(X, H, L, member1_in_gg(X, L))
MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)
U2_GGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_ag(Y, L))
U2_GGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → MEMBER_IN_AG(Y, L)
MEMBER_IN_AG(X, .(H, L)) → U6_AG(X, H, L, member_in_ag(X, L))
MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)
U3_GGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U3_GGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → DELETE_IN_AGA(Y, L, V1)
DELETE_IN_AGA(X, .(H, T1), .(H, T2)) → U8_AGA(X, H, T1, T2, delete_in_aga(X, T1, T2))
DELETE_IN_AGA(X, .(H, T1), .(H, T2)) → DELETE_IN_AGA(X, T1, T2)
U4_GGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_GGGG(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → REACH_IN_AGGG(Y, Z, E, V1)
REACH_IN_AGGG(X, Y, E, L) → U1_AGGG(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
REACH_IN_AGGG(X, Y, E, L) → MEMBER_IN_GG(.(X, .(Y, [])), E)
REACH_IN_AGGG(X, Z, E, L) → U2_AGGG(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
REACH_IN_AGGG(X, Z, E, L) → MEMBER1_IN_GG(.(X, .(Y, [])), E)
U2_AGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_AGGG(X, Z, E, L, Y, member_in_ag(Y, L))
U2_AGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → MEMBER_IN_AG(Y, L)
U3_AGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_AGGG(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U3_AGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → DELETE_IN_AGA(Y, L, V1)
U4_AGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_AGGG(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U4_AGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → REACH_IN_AGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)
U4_AGGG(x1, x2, x3, x4, x5, x6)  =  U4_AGGG(x2, x3, x6)
U2_GGGG(x1, x2, x3, x4, x5)  =  U2_GGGG(x2, x3, x4, x5)
U5_AGGG(x1, x2, x3, x4, x5)  =  U5_AGGG(x5)
U6_GG(x1, x2, x3, x4)  =  U6_GG(x4)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
REACH_IN_GGGG(x1, x2, x3, x4)  =  REACH_IN_GGGG(x1, x2, x3, x4)
U1_GGGG(x1, x2, x3, x4, x5)  =  U1_GGGG(x5)
U3_GGGG(x1, x2, x3, x4, x5, x6)  =  U3_GGGG(x2, x3, x4, x6)
U8_AGA(x1, x2, x3, x4, x5)  =  U8_AGA(x5)
U5_GGGG(x1, x2, x3, x4, x5)  =  U5_GGGG(x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
U7_GG(x1, x2, x3, x4)  =  U7_GG(x4)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x4)
DELETE_IN_AGA(x1, x2, x3)  =  DELETE_IN_AGA(x2)
U4_GGGG(x1, x2, x3, x4, x5, x6)  =  U4_GGGG(x2, x3, x6)
U1_AGGG(x1, x2, x3, x4, x5)  =  U1_AGGG(x5)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 5 SCCs with 20 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN_AGA(X, .(H, T1), .(H, T2)) → DELETE_IN_AGA(X, T1, T2)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)
DELETE_IN_AGA(x1, x2, x3)  =  DELETE_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

DELETE_IN_AGA(X, .(H, T1), .(H, T2)) → DELETE_IN_AGA(X, T1, T2)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
DELETE_IN_AGA(x1, x2, x3)  =  DELETE_IN_AGA(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

DELETE_IN_AGA(.(T1)) → DELETE_IN_AGA(T1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(X, .(H, L)) → MEMBER_IN_AG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_AG(.(L)) → MEMBER_IN_AG(L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(H, L)) → MEMBER1_IN_GG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER1_IN_GG(x1, x2)  =  MEMBER1_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER1_IN_GG(X, .(L)) → MEMBER1_IN_GG(X, L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_IN_GG(X, .(L)) → MEMBER_IN_GG(X, L)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U3_AGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_AGGG(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_AGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → REACH_IN_AGGG(Y, Z, E, V1)
REACH_IN_AGGG(X, Z, E, L) → U2_AGGG(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_AGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_AGGG(X, Z, E, L, Y, member_in_ag(Y, L))

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_ag(Y, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))
U3_gggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
reach_in_aggg(X, Y, E, L) → U1_aggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
U1_aggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_aggg(X, Y, E, L)
reach_in_aggg(X, Z, E, L) → U2_aggg(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_aggg(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_aggg(X, Z, E, L, Y, member_in_ag(Y, L))
U3_aggg(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_aggg(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_aggg(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → U5_aggg(X, Z, E, L, reach_in_aggg(Y, Z, E, V1))
U5_aggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_aggg(X, Z, E, L)
U5_gggg(X, Z, E, L, reach_out_aggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4)  =  reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5)  =  U1_gggg(x5)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
.(x1, x2)  =  .(x2)
member_out_gg(x1, x2)  =  member_out_gg
U6_gg(x1, x2, x3, x4)  =  U6_gg(x4)
[]  =  []
reach_out_gggg(x1, x2, x3, x4)  =  reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5)  =  U2_gggg(x2, x3, x4, x5)
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
U3_gggg(x1, x2, x3, x4, x5, x6)  =  U3_gggg(x2, x3, x4, x6)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U4_gggg(x1, x2, x3, x4, x5, x6)  =  U4_gggg(x2, x3, x6)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U5_gggg(x1, x2, x3, x4, x5)  =  U5_gggg(x5)
reach_in_aggg(x1, x2, x3, x4)  =  reach_in_aggg(x2, x3, x4)
U1_aggg(x1, x2, x3, x4, x5)  =  U1_aggg(x5)
reach_out_aggg(x1, x2, x3, x4)  =  reach_out_aggg
U2_aggg(x1, x2, x3, x4, x5)  =  U2_aggg(x2, x3, x4, x5)
U3_aggg(x1, x2, x3, x4, x5, x6)  =  U3_aggg(x2, x3, x4, x6)
U4_aggg(x1, x2, x3, x4, x5, x6)  =  U4_aggg(x2, x3, x6)
U5_aggg(x1, x2, x3, x4, x5)  =  U5_aggg(x5)
U4_AGGG(x1, x2, x3, x4, x5, x6)  =  U4_AGGG(x2, x3, x6)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U3_AGGG(X, Z, E, L, Y, member_out_ag(Y, L)) → U4_AGGG(X, Z, E, L, Y, delete_in_aga(Y, L, V1))
U4_AGGG(X, Z, E, L, Y, delete_out_aga(Y, L, V1)) → REACH_IN_AGGG(Y, Z, E, V1)
REACH_IN_AGGG(X, Z, E, L) → U2_AGGG(X, Z, E, L, member1_in_gg(.(X, .(Y, [])), E))
U2_AGGG(X, Z, E, L, member1_out_gg(.(X, .(Y, [])), E)) → U3_AGGG(X, Z, E, L, Y, member_in_ag(Y, L))

The TRS R consists of the following rules:

delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(H, T1), .(H, T2)) → U8_aga(X, H, T1, T2, delete_in_aga(X, T1, T2))
member1_in_gg(H, .(H, L)) → member1_out_gg(H, .(H, L))
member1_in_gg(X, .(H, L)) → U7_gg(X, H, L, member1_in_gg(X, L))
member_in_ag(H, .(H, L)) → member_out_ag(H, .(H, L))
member_in_ag(X, .(H, L)) → U6_ag(X, H, L, member_in_ag(X, L))
U8_aga(X, H, T1, T2, delete_out_aga(X, T1, T2)) → delete_out_aga(X, .(H, T1), .(H, T2))
U7_gg(X, H, L, member1_out_gg(X, L)) → member1_out_gg(X, .(H, L))
U6_ag(X, H, L, member_out_ag(X, L)) → member_out_ag(X, .(H, L))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
[]  =  []
member1_in_gg(x1, x2)  =  member1_in_gg(x1, x2)
member1_out_gg(x1, x2)  =  member1_out_gg
U7_gg(x1, x2, x3, x4)  =  U7_gg(x4)
member_in_ag(x1, x2)  =  member_in_ag(x2)
member_out_ag(x1, x2)  =  member_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
delete_in_aga(x1, x2, x3)  =  delete_in_aga(x2)
delete_out_aga(x1, x2, x3)  =  delete_out_aga(x3)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
U4_AGGG(x1, x2, x3, x4, x5, x6)  =  U4_AGGG(x2, x3, x6)
U2_AGGG(x1, x2, x3, x4, x5)  =  U2_AGGG(x2, x3, x4, x5)
U3_AGGG(x1, x2, x3, x4, x5, x6)  =  U3_AGGG(x2, x3, x4, x6)
REACH_IN_AGGG(x1, x2, x3, x4)  =  REACH_IN_AGGG(x2, x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REACH_IN_AGGG(Z, E, L) → U2_AGGG(Z, E, L, member1_in_gg(.(.([])), E))
U2_AGGG(Z, E, L, member1_out_gg) → U3_AGGG(Z, E, L, member_in_ag(L))
U4_AGGG(Z, E, delete_out_aga(V1)) → REACH_IN_AGGG(Z, E, V1)
U3_AGGG(Z, E, L, member_out_ag) → U4_AGGG(Z, E, delete_in_aga(L))

The TRS R consists of the following rules:

delete_in_aga(.(Y)) → delete_out_aga(Y)
delete_in_aga(.(T1)) → U8_aga(delete_in_aga(T1))
member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U7_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U6_ag(member_in_ag(L))
U8_aga(delete_out_aga(T2)) → delete_out_aga(.(T2))
U7_gg(member1_out_gg) → member1_out_gg
U6_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

delete_in_aga(x0)
member1_in_gg(x0, x1)
member_in_ag(x0)
U8_aga(x0)
U7_gg(x0)
U6_ag(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


REACH_IN_AGGG(Z, E, L) → U2_AGGG(Z, E, L, member1_in_gg(.(.([])), E))
The remaining pairs can at least be oriented weakly.

U2_AGGG(Z, E, L, member1_out_gg) → U3_AGGG(Z, E, L, member_in_ag(L))
U4_AGGG(Z, E, delete_out_aga(V1)) → REACH_IN_AGGG(Z, E, V1)
U3_AGGG(Z, E, L, member_out_ag) → U4_AGGG(Z, E, delete_in_aga(L))
Used ordering: Polynomial interpretation [25]:

POL(.(x1)) = 1 + x1   
POL(REACH_IN_AGGG(x1, x2, x3)) = 1 + x3   
POL(U2_AGGG(x1, x2, x3, x4)) = x3   
POL(U3_AGGG(x1, x2, x3, x4)) = x3   
POL(U4_AGGG(x1, x2, x3)) = x3   
POL(U6_ag(x1)) = 0   
POL(U7_gg(x1)) = 0   
POL(U8_aga(x1)) = 1 + x1   
POL([]) = 0   
POL(delete_in_aga(x1)) = x1   
POL(delete_out_aga(x1)) = 1 + x1   
POL(member1_in_gg(x1, x2)) = 0   
POL(member1_out_gg) = 0   
POL(member_in_ag(x1)) = 0   
POL(member_out_ag) = 0   

The following usable rules [17] were oriented:

delete_in_aga(.(Y)) → delete_out_aga(Y)
U8_aga(delete_out_aga(T2)) → delete_out_aga(.(T2))
delete_in_aga(.(T1)) → U8_aga(delete_in_aga(T1))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

U2_AGGG(Z, E, L, member1_out_gg) → U3_AGGG(Z, E, L, member_in_ag(L))
U3_AGGG(Z, E, L, member_out_ag) → U4_AGGG(Z, E, delete_in_aga(L))
U4_AGGG(Z, E, delete_out_aga(V1)) → REACH_IN_AGGG(Z, E, V1)

The TRS R consists of the following rules:

delete_in_aga(.(Y)) → delete_out_aga(Y)
delete_in_aga(.(T1)) → U8_aga(delete_in_aga(T1))
member1_in_gg(H, .(L)) → member1_out_gg
member1_in_gg(X, .(L)) → U7_gg(member1_in_gg(X, L))
member_in_ag(.(L)) → member_out_ag
member_in_ag(.(L)) → U6_ag(member_in_ag(L))
U8_aga(delete_out_aga(T2)) → delete_out_aga(.(T2))
U7_gg(member1_out_gg) → member1_out_gg
U6_ag(member_out_ag) → member_out_ag

The set Q consists of the following terms:

delete_in_aga(x0)
member1_in_gg(x0, x1)
member_in_ag(x0)
U8_aga(x0)
U7_gg(x0)
U6_ag(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 3 less nodes.